{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
  UndecidableInstances, TemplateHaskell, QuasiQuotes, TypeOperators #-}

{-# OPTIONS_GHC -fcontext-stack=200 #-}

{- |

Module      :  Examples.TermInner
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

A let-elaboration via "Data.Yoko.InDT".

-}
module Examples.TermInner where

import Examples.TermBase
import Examples.InnerBase (Inner)
import qualified Examples.InnerBase as I
import qualified Examples.TermGeneric as G
import Examples.InnerGeneric ()

import Data.Yoko



elaborate :: Term -> Inner; elaborate = apply $ Elab `atM2` [qP|IdM|]

data Elab m t = Elab; wraps_trivially ''Elab

type instance t ::? Domain (Elab IdM) = t ::? (:=:) Term
type instance Dom (Elab m) t = Med m t
type instance Rng (Elab m) t = Med m (TApp (Elab m) t)
type instance TApp (Elab m) Term = Inner

instance (IdM ~ m) => Term ::: Domain (Elab m) where
  membership = AppBy $ \_ -> dcDispatch $
    weakenOrNT (one elab_Let) $ NT $ imageInDTU Elab

elab_Let (G.Let ds tm) =
  foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds





ex0 = Let [Decl TInt (Var 111), Decl TBool (Var 222)] (Var 0)

ex1 = elaborate ex0
